/**
 * Algebraic Decision Diagram Package
 * 
 * @author Scott Sanner (ssanner@gmail.com)
 * @version 7/25/03
 *
 **/

package dd.discrete;

import graph.Graph;

import util.MapList;
import util.Pair;

import java.io.*;
import java.math.*;
import java.text.*;
import java.util.*;

/**
 * General class for implementation of ADD data structure
 **/
public class ADD extends DD {

	public final static double NEGINF = -123456d;
	
	// Internal statistics
	public static long APPLY_CALLS = 0;
	public static int OR_PRUNE_CNT = 0;
	public static int AND_PRUNE_CNT = 0;
	public static int PROD_PRUNE_CNT = 0;
	public static int MIN_PRUNE_CNT = 0;
	public static int MAX_PRUNE_CNT = 0;
	public static int PRECISION_PRUNES = 0;
	public static int PRUNE_CACHE_HITS = 0;

	// Local data for ADD
	public long _nLocalIDCnt; // counter for local ids
	public HashMap<Long, ADDNode> _hmADDNodes; // int -> ADDNode
	public HashMap<SNodePair, Long> _hmPairs; // <ADD-v1-id, ADD-v2-id> -> ADDNode (for ADD-3)
	// (Apply cache)
	public HashMap<Long, ADDNode> _hmReduceMap; // <id-of-node-to-reduce> -> ADDNode (reduced)
	public HashMap<Long, Long> _hmPruneMap; // map of node prunes
	public HashMap<SINodeIndex, ADDINode> _hmINodeCache; // <global-id, low, high> -> ADDINode
	public HashMap<SDNodeIndex, ADDDNode> _hmDNodeCache; // <min-val, max-val> -> ADDDNode

	private HashMap<SINodeIndex, ADDINode> _hmTempINodes;
	private HashMap<SDNodeIndex, ADDDNode> _hmTempDNodes;
	private HashMap<Long, ADDNode> _hmTempADDNodes;
	/*
	 * Checklist for removing ADDRNode
	 * -_hmADDNodes should have ints
	 * -_hsSpecialNodes has ints
	 * -retain these ints while flushing
	 * -do not create new objects
	 * -check correct type object added to _hmINodeCache, _hmDNodeCache, _hmReduceMap, _hmADDNodes
	 */
	
	public Map<Pair<Long, Double>, Long> threshCache
		= new HashMap<Pair<Long, Double>, Long>();

	public int	threshHit = 0;

	private Map<Long, Long>	alignCache = new HashMap<Long, Long>();

	private HashMap<Long, Long> constrainRestrictCache = new HashMap<Long, Long>();

	public int constrainHit = 0 ;


	// /////////////////////////////////////////////////////////////////
	// Basic and copy constructors
	// /////////////////////////////////////////////////////////////////

	public ADD(ArrayList<Integer> order) {

		_nLocalIDCnt = 0;
		
	    _alOrder = new ArrayList<Integer>();
	    
	    for (int i = 0; i < order.size(); i++) {
	    	Integer var_id = i + 1;
	    	_alOrder.add(var_id);
	    }
		
		_hmADDNodes = new HashMap<Long, ADDNode>();
		_hmGVarToLevel = new HashMap<Integer, Integer>();
		_hmPairs = new HashMap<SNodePair, Long>();
		_hmReduceMap = new HashMap<Long, ADDNode>();
		_hmPruneMap = new HashMap<Long, Long>();
		_hmINodeCache = new HashMap<SINodeIndex, ADDINode>();
		_hmDNodeCache = new HashMap<SDNodeIndex, ADDDNode>();

		// Build map from global var to order level
		_hmGVarToLevel.clear();
		for (int i = 0; i < _alOrder.size(); i++) {
			_hmGVarToLevel.put(_alOrder.get(i), new Integer(i));
		}
	}

	// ////////////////////////////////////////////////////////////////
	// Flushing and special node maintenance
	// ////////////////////////////////////////////////////////////////

	// Flush caches but save special nodes
	public void flushCaches(boolean print_info) {

		// Print starting info
		if (print_info) {
//			System.out.print("[FLUSHING CACHES... ");
//			 showCacheSize();
//			ResetTimer();
		}

		_hmPairs.clear();
		_hmReduceMap.clear();
		_hmPruneMap.clear();

		_hmTempADDNodes = new HashMap<Long, ADDNode>();
		_hmTempINodes = new HashMap<SINodeIndex, ADDINode>();
		_hmTempDNodes = new HashMap<SDNodeIndex, ADDDNode>();
		
		// Copy over 'special' nodes then set new maps
		Iterator<Integer> i = _hsSpecialNodes.iterator();
		while (i.hasNext()) {
			cacheNode(i.next());
		}
		
		_hmADDNodes.clear();
		_hmINodeCache.clear();
		_hmDNodeCache.clear();
		
		_hmADDNodes = _hmTempADDNodes;
		_hmINodeCache = _hmTempINodes;
		_hmDNodeCache = _hmTempDNodes;

		// Print results
		if (GC_DURING_FLUSH) {
			RUNTIME.gc();
		}
		if (print_info) {
//			System.out.print(" TIME: " + GetElapsedTime());
//			System.out.print("  RESULT: "
//							+ _df.format(((double) RUNTIME.freeMemory() 
//									      / (double) RUNTIME.totalMemory())));
//			System.out.print("  CACHE: " + getCacheSize() + "] ");
		}
	}

	public void cacheNode(long dd) {
		
		if (_hmTempADDNodes.containsKey(dd)) {
			return;
		}
		
		ADDNode n = getNode(dd);
		
		_hmTempADDNodes.put(dd, n);
		
		_hmADDNodes.remove(dd);
		
		if (n instanceof ADDINode) {
			ADDINode ni = (ADDINode) n;
			SINodeIndex sindex = new SINodeIndex(ni._nTestVarID, ni._nLow,
					ni._nHigh);
			
			_hmTempINodes.put( sindex, ni);
			
			_hmINodeCache.remove(sindex);
			
			cacheNode(ni._nLow);
			cacheNode(ni._nHigh);
			
		} else if (n instanceof ADDDNode) {
			ADDDNode d = (ADDDNode) n;
			SDNodeIndex sdindex = new SDNodeIndex(d._dLower, d._dUpper);
			
			_hmTempDNodes.put( sdindex, d);
			
			_hmDNodeCache.remove(sdindex);
			
		}
		
	}

	// ////////////////////////////////////////////////////////////////
	// Internal data structure maintenance
	// ////////////////////////////////////////////////////////////////

	// Quick cache snapshot
	public void showCacheSize() {
		System.out.println("APPLY CACHE:  " + _hmPairs.size());
		System.out.println("REDUCE CACHE: " + _hmReduceMap.size());
		System.out.println("INODE CACHE:  " + _hmINodeCache.size() + "\n");
	}

	// Total cache snapshot
	public long getCacheSize() {
		return _hmPairs.size() + _hmReduceMap.size() + _hmINodeCache.size();
	}

	// An exact count for the ADD rooted at _nRoot
	public long countExactNodes(long id) {
		Set<Long> cset = new HashSet<Long>();
		countExactNodesInt(cset, id);
		return cset.size();
	}

	public Set<Long> getExactNodes(long id) {
		HashSet<Long> cset = new HashSet<Long>();
		countExactNodesInt(cset, id);
		return cset;
	}

	public void countExactNodesInt(Set<Long> cset, long id) {
		if (cset.contains(id) ) {
			return;
		}
		
		ADDNode n = getNode(id);
		 
		//Uncomment the following to get internal-only count
		if (n instanceof ADDDNode) {
			return;
		}
		 
		cset.add(id);
		
		if (n instanceof ADDINode) {
			countExactNodesInt(cset, ((ADDINode) n)._nLow);
			countExactNodesInt(cset, ((ADDINode) n)._nHigh);
		}
		
	}

	public Set<Integer> getGIDs(int id) {
		Set<Long> cset = new TreeSet<Long>();
		Set<Integer> gset = new TreeSet<Integer>();
		collectGIDsInt(cset, gset, id);
		return gset;
	}

	public void collectGIDsInt(Set<Long> cset, Set<Integer> gset, long id) {
		if (cset.contains(id) ) {
			return;
		}
		
		cset.add(id);
		
		ADDNode n = getNode(id);
		if (n instanceof ADDINode) {
			ADDINode inode = ((ADDINode) n);
			gset.add( inode._nTestVarID);
			collectGIDsInt(cset, gset, inode._nLow);
			collectGIDsInt(cset, gset, inode._nHigh);
		}
	}

	// ////////////////////////////////////////////////////////////////
	// Node maintenance
	// ////////////////////////////////////////////////////////////////

	// The only way to retrieve an actual ADDNode!!!
	public ADDNode getNode(long local_id) {
		if (local_id >= 0 && local_id < _nLocalIDCnt) {
			return _hmADDNodes.get(local_id);
		} else {
			return null;
		}
	}

	public long createINode(int gid, long low, long high) {

		// System.out.println("Create: <" + gid + "," + low + "," + high +
		// ">  ->  " + _nLocalIDCnt);

		SINodeIndex sindex = new SINodeIndex(gid, low, high);
		
		if( _hmADDNodes.containsKey(sindex) ){
			return _hmADDNodes.get(sindex)._nLocalID;
		}else{
			long lid = _nLocalIDCnt++;
			ADDINode n = new ADDINode(lid, gid, low, high);
			
			_hmADDNodes.put(lid, n);
			_hmINodeCache.put( sindex, n);

			return lid;
	
		}
		
	}

	public long createDNode(double min_val, double max_val) {
		return createDNode(min_val, max_val, null, null);
	}

	public long createDNode(double min_val, double max_val, 
			String lower_label, String upper_label) {

		SDNodeIndex sdindex = new SDNodeIndex(min_val, max_val);
		
		if( _hmDNodeCache.containsKey(sdindex) ){
			return _hmDNodeCache.get(sdindex)._nLocalID;
		}else{
			long lid = _nLocalIDCnt++;
			ADDDNode n = new ADDDNode(lid, min_val, max_val, lower_label,
					upper_label);
			_hmADDNodes.put(lid, n);
			_hmDNodeCache.put(sdindex, n );

			return lid;	
		}
		
		
	}

	// This actually does low==high simplification in place... very
	// important to ensure ref counts ok since double linking screws
	// things up. WARNING: May not return INode if low==high.
	public long getINode(int gid, long low, long high, boolean create) {

		// First check if low == high... in this case, just perform the
		// obvious equivalent reduction (this saves headaches later)
		if (low == high) {
			return low;
		}

		SINodeIndex index = new SINodeIndex(gid, low, high);
		
		if( _hmINodeCache.containsKey(index) ){
			ADDINode inode = _hmINodeCache.get(index);
			return inode._nLocalID;
		}
		
		if (create) {
			return createINode(gid, low, high);
		} else {
			return INVALID;
		}
		
	}

	public long getDNode(double min_val, double max_val, boolean create) {
		return getDNode(min_val, max_val, create, min_val+"", max_val+"");
	}

	public long getDNode(double min_val, double max_val, boolean create,
			String lower_label, String upper_label) {
		
		SDNodeIndex index = new SDNodeIndex(min_val, max_val);
		
		if( _hmDNodeCache.containsKey(index) ){
			return _hmDNodeCache.get(index)._nLocalID;
		}
		
		if (create) {
			return createDNode(min_val, max_val, lower_label, upper_label);
		} else {
			return INVALID;
		}
		
	}

	public void putPair(long id1, long id2, int op, long to_id) {
		_hmPairs.put(new SNodePair(id1, id2, op), to_id);
	}

	public long getPair(long id1, long id2, int op) {
		
		SNodePair index = new SNodePair(id1, id2, op);
		
		if( _hmPairs.containsKey(index) ){
			return _hmPairs.get(index);
		}
		
		return INVALID;
		
	}

	// For terminal node labelling - not involved in computation
//	public void setAllDNodeLabels(String lower, String upper) {
//		Iterator i = ((Set) _hmDNodeCache.entrySet()).iterator();
//		while (i.hasNext()) {
//			Map.Entry me = (Map.Entry) i.next();
//			ADDRNode id = (ADDRNode) me.getValue();
//			ADDDNode d = (ADDDNode) getNode(id._lid);
//			d._sLowerLabel = lower;
//			d._sUpperLabel = upper;
//		}
//	}

	// Set the min/max values for node given by id
	public void setMinMax(long id) {
		Set<Long> setted = new HashSet<Long>();
		setMinMaxInt(id, setted);
	}

	private void setMinMaxInt(long id, Set<Long> setted){
		
		if( setted.contains(id) == true ){
			return;
		}
		
		ADDNode node = getNode(id);
		
		if( node instanceof ADDDNode ){
			return;
		}
		
		ADDINode ni = (ADDINode) node;
		
		ADDNode l = getNode(ni._nLow);
		ADDNode h = getNode(ni._nHigh);

		double ldmin_lower, ldmin_upper, ldmax_lower, ldmax_upper;
		double hdmin_lower, hdmin_upper, hdmax_lower, hdmax_upper;

		// Determine values for low node
		if (l instanceof ADDINode) {
			
			if( ! setted.contains(ni._nLow) ){
				setMinMax(ni._nLow);
			}
			
			ldmin_lower = ((ADDINode) l)._dMinLower;
			ldmin_upper = ((ADDINode) l)._dMinUpper;
			ldmax_lower = ((ADDINode) l)._dMaxLower;
			ldmax_upper = ((ADDINode) l)._dMaxUpper;
			
		} else if (l instanceof ADDDNode) {
			ldmin_lower = ldmax_lower = ((ADDDNode) l)._dLower;
			ldmin_upper = ldmax_upper = ((ADDDNode) l)._dUpper;
		} else {
			ldmin_lower = ldmin_upper = ldmax_lower = ldmax_upper = Double.NaN;
		}

		// Determine values for high node
		if (h instanceof ADDINode) {
			
			if( ! setted.contains(ni._nHigh) ){
				setMinMax(ni._nHigh);
			}
			
			hdmin_lower = ((ADDINode) h)._dMinLower;
			hdmin_upper = ((ADDINode) h)._dMinUpper;
			hdmax_lower = ((ADDINode) h)._dMaxLower;
			hdmax_upper = ((ADDINode) h)._dMaxUpper;
		} else if (h instanceof ADDDNode) {
			hdmin_lower = hdmax_lower = ((ADDDNode) h)._dLower;
			hdmin_upper = hdmax_upper = ((ADDDNode) h)._dUpper;
		} else {
			hdmin_lower = hdmin_upper = hdmax_lower = hdmax_upper = Double.NaN;
		}

		// Set min/max values for ni (first is fn, second is lower,upper)
		ni._dMinLower = Math.min(ldmin_lower, hdmin_lower);
		ni._dMinUpper = Math.min(ldmin_upper, hdmin_upper);
		ni._dMaxLower = Math.max(ldmax_lower, hdmax_lower);
		ni._dMaxUpper = Math.max(ldmax_upper, hdmax_upper);
	}
	// ///////////////////////////////////////////////////////////////
	// General ADD operations
	// ///////////////////////////////////////////////////////////////

	// Get min for a generic node
	public double getMin(long id) {
		ADDNode n = getNode(id);
		if (n instanceof ADDINode) {
			ADDINode in = (ADDINode) n;
			return in._dMinLower;
		} else if (n instanceof ADDDNode) {
			ADDDNode dn = (ADDDNode) n;
			return dn._dLower;
		} else {
			return Double.NEGATIVE_INFINITY;
		}
	}

	// Get max for a generic node
	public double getMax(long id) {
		ADDNode n = getNode(id);
		if (n instanceof ADDINode) {
			ADDINode in = (ADDINode) n;
			return in._dMaxUpper;
		} else if (n instanceof ADDDNode) {
			ADDDNode dn = (ADDDNode) n;
			return dn._dUpper;
		} else {
			return Double.POSITIVE_INFINITY;
		}
	}

	// Assuming the difference has already taken place, this method
	// finds the maximum difference
	// TODO: Make this work with ADDSNode... only used for FOMDP epsilon
	// convergence
//	public double getMaxAbsValue() {
//
//		double max_diff = Double.NEGATIVE_INFINITY;
//
//		// Get all DNodes, negate, make a new cache and replace old cache
//		HashMap new_dnode_cache = new HashMap();
//		Iterator i = _hmDNodeCache.keySet().iterator();
//		while (i.hasNext()) {
//			SDNodeIndex dni = (SDNodeIndex) i.next();
//
//			double upper = (dni._dUpperVal < 0) ? -dni._dUpperVal
//					: dni._dUpperVal;
//			double lower = (dni._dLowerVal < 0) ? -dni._dLowerVal
//					: dni._dLowerVal;
//
//			if (max_diff < upper) {
//				max_diff = upper;
//			}
//
//			if (max_diff < lower) {
//				max_diff = lower;
//			}
//		}
//
//		// Return max diff
//		return max_diff;
//	}

//	public double getMaxValue(long id) {
//
//		ADDNode root = getNode(id);
//		if (root instanceof ADDDNode) {
//			return ((ADDDNode) root)._dUpper;
//		} else {
//			return ((ADDINode) root)._dMaxUpper;
//		}
//	}
//
//	// Find the minimum value in an ADD (must be on the lower val)
//	public double getMinValue(int id) {
//
//		ADDNode root = getNode(id);
//		if (root instanceof ADDDNode) {
//			return ((ADDDNode) root)._dLower;
//		} else {
//			return ((ADDINode) root)._dMinLower;
//		}
//	}

	// Complements the terminal BNodes in an ADD
//	public ADD complementInPlace() {
//
//		// Swap BNode true and false and update BNodeCache
//		int prevTrue = _aBNodeCache[1];
//		int prevFalse = _aBNodeCache[0];
//
//		if (prevTrue > INVALID) {
//			((ADDBNode) getNode(prevTrue))._bVal = false;
//		}
//		if (prevFalse > INVALID) {
//			((ADDBNode) getNode(prevFalse))._bVal = true;
//		}
//
//		_aBNodeCache[1] = prevFalse;
//		_aBNodeCache[0] = prevTrue;
//
//		return this;
//	}

	// Returns a new ADD with scalar multiplication of terminal nodes
	public long scalarMultiply(long id, double val) {
		return scalarMultiply(id, val, val);
	}

	public long scalarMultiply(long id, double val_lower, double val_upper) {
		long d = getDNode(val_lower, val_upper, true);
		return applyInt(id, d, ARITH_PROD);
	}

	public long scalarAdd(long id, double val) {
		long d = getDNode(val, val, true);
		return applyInt(id, d, ARITH_SUM);
	}

	public long negate(long id) {
		long d = getDNode(0d, 0d, true);
		return applyInt(d, id, ARITH_MINUS);
	}

	public long invert(long id) {
		long d = getDNode(1d, 1d, true);
		return applyInt(d, id, ARITH_DIV);
	}

	public long APRICODD( long id ){
		
		TreeSet<ADDDNode> nodes = new TreeSet<ADDDNode>();
		
		collectLeaves(id, nodes, new HashSet<ADDINode>());
		
		System.out.println(nodes);
		
		return APRICODDInt(id, new HashMap<Long, Long>(), nodes, );
	}
	// /////////////////////////////////////////////////////////////////////////
	// Approximation Algorithms
	// /////////////////////////////////////////////////////////////////////////

	// Start at root
//	public long pruneNodes(long id) {
//
//		if (PRUNE_TYPE == NO_REPLACE || PRUNE_PRECISION <= 0d){
//			return id;
//		}
//
//		if ( (PRUNE_TYPE != REPLACE_AVG && PRUNE_TYPE != REPLACE_MIN && 
//				PRUNE_TYPE != REPLACE_MAX && PRUNE_TYPE != REPLACE_AVG ) ) {
//			System.out.println("Illegal ADD replacement type " + PRUNE_TYPE);
//			System.exit(1);
//		}
//
//		HashSet<ADDDNode> leaves = new HashSet<ADDDNode>();
//		collectLeaves(id, leaves);
//		//System.out.println(leaves);
//		HashMap<Long, Long> remap = compressLeaves(leaves);
//		//System.out.println(remap);
//		//System.exit(1);
//		return reduceRemapLeaves(id, remap);
//	}
//
//	public long reduceRemapLeaves(long id, HashMap<Long, Long> remap) {
//		_hmPruneMap.clear();
//		return reduceRemapLeaves2(id, remap);
//	}
//	
//	public long reduceRemapLeaves2(long id, HashMap<Long, Long> remap) {
//		// Have we examined this node id already?
//		// System.out.println("Reduce(" + id + ")");
//		if ( _hmPruneMap.containsKey(id) ){
//			// System.out.println("In cache, returning: " + qret);
//			return _hmPruneMap.get(id);
//		}
//
//		// Proceed with reduction algorithm
//		// System.out.println("Not in cache");
//		long ret = INVALID;
//		ADDNode n = getNode(id);
//
//		// Update caches and reduce if needed
//		if (n instanceof ADDDNode) {
//			ADDDNode dn = (ADDDNode) n;
//			
//			if( remap.containsKey(dn._nLocalID) ){
//				long remapid = remap.get(dn._nLocalID);
//				ADDDNode remap_dnode = (ADDDNode)getNode(remapid);
//				ret = remap_dnode._nLocalID;					
//			}else{
//				ret = getDNode(dn._dLower, dn._dUpper, true, dn._sLowerLabel,
//						dn._sUpperLabel);
//			}
//		} else { // n instanceof ADDINode so recurse and update caches
//			ADDINode ni = (ADDINode) n;
//
//			// Get new low and high branches
//			long low = reduceRemapLeaves2(ni._nLow, remap);
//			long high = reduceRemapLeaves2(ni._nHigh, remap);
//
//			// Don't recursively delete if low==high since low
//			// will be reused although it may not be linked yet.
//			// And we know that low will *have* to be used.
//
//			// Decide which node to return (takes care of 'low==high' case)
//			// System.out.println("Get:    <" + ni._nGlobalID + "," + low +
//			// "," + high + ">");
//			ret = getINode(ni._nTestVarID, low, high, true);
//			// System.out.println("Result: <" + ni._nGlobalID + "," + low +
//			// "," + high + ">  ->  " + ret);
//
//			// getINode may return a DNode or BNode if low==high
//			if (getNode(ret) instanceof ADDINode) {
//				setMinMax(ret);
//			}
//		}
//
//		_hmPruneMap.put(id, ret);
//
//		return ret;
//	}
//
	public void collectLeaves(long id, TreeSet<ADDDNode> nodes, HashSet<ADDINode> examined) {
		
		ADDNode n = getNode(id);
		if (n instanceof ADDDNode) {
			nodes.add((ADDDNode) n);
		} else {
			ADDINode ni = (ADDINode) n;
			
			if( examined.contains(ni) ){
				return;
			}
			
			collectLeaves(ni._nLow, nodes, examined);
			collectLeaves(ni._nHigh, nodes, examined);
			
			examined.add(ni);
			
		}
	}
//
//	public HashMap<Long, Long> compressLeaves(TreeSet<ADDDNode> leaves) {
//
//		 collect = new ArrayList();
//		MapList remap = new MapList(false, true /*hash*/);
//		double MERGE_PRECISION = PRUNE_PRECISION / 2d;
//
//		// Collect all distinct leaves... if approximate match in 
//		// 'collect' then make note in map, otherwise add it to 'collect'
//		Iterator i = leaves.iterator();
//		collect.clear();
//		collect.add((ADDDNode) i.next());
//		while (i.hasNext()) {
//			ADDDNode d1 = (ADDDNode) i.next();
//			for (Iterator j = collect.iterator(); d1 != null && j.hasNext();) {
//				ADDDNode d2 = (ADDDNode) j.next();
//				if (Math.abs(d1._dLower - d2._dLower) <= MERGE_PRECISION) {
//					remap.putValue(d2, d1); // common node -> mapped node
//					d1 = null;
//				}
//			}
//			if (d1 != null)
//				collect.add(d1);
//		}
//
//		// Now build HashMap to remap
//		i = collect.iterator();
//		HashMap ret_map = new HashMap();
//		while (i.hasNext()) {
//			ADDDNode common = (ADDDNode) i.next();
//			ArrayList remapped = remap.getValues(common);
//			double replace_val = common._dLower;
//			double minmax = common._dLower;
//			for (Iterator j = remapped.iterator(); j.hasNext();) {
//				ADDDNode d = (ADDDNode) j.next();
//				replace_val += d._dLower;
//				minmax = (PRUNE_TYPE == REPLACE_MAX) ? Math.max(minmax,
//						d._dLower) : Math.min(minmax, d._dLower);
//			}
//			if (PRUNE_TYPE == REPLACE_AVG)
//				replace_val /= (double) (1 + remapped.size());
//			else if (PRUNE_TYPE == REPLACE_MAX || PRUNE_TYPE == REPLACE_MIN)
//				replace_val = minmax;
//			else {
//				System.out.println("Illegal ADD prune type: " + PRUNE_TYPE);
//				System.exit(1);
//			}
//
//			ADDDNode new_dnode = (ADDDNode) this.getNode(this.getDNode(
//					replace_val, replace_val, true));
//			ret_map.put(common, new_dnode);
//			for (Iterator j = remapped.iterator(); j.hasNext();)
//				ret_map.put(((ADDDNode) j.next()), new_dnode);
//		}
//
//		return ret_map;
//	}
//
//	// Prunes all node structure having impact less than prune_precision.
//	// Range included because need a measure of the range induced by the
//	// error at the node.
//	public int pruneNodes(int id, boolean recurse) {
//
//		// Can immediately check for local ID of 0
//		ADDNode n = getNode(id);
//		if (n instanceof ADDDNode) {
//			return id;
//		}
//
//		ADDINode ni = (ADDINode) n;
//		double range = ni._dMaxUpper - ni._dMinLower;
//
//		// Check for a range below precision
//		if (range <= PRUNE_PRECISION) {
//
//			// This entire subtree has impact less than prune_precision
//			// Note: Not making use of DNode ranges here!!! A single
//			// ADD can only have one leaf value in this framework,
//			// not a range.
//			switch (PRUNE_TYPE) {
//			case NO_REPLACE:
//			case REPLACE_LOW:
//			case REPLACE_HIGH: {
//			}
//				break;
//			case REPLACE_MIN: {
//				return getDNode(ni._dMinLower, ni._dMinLower, true);
//			}
//			case REPLACE_MAX: {
//				return getDNode(ni._dMaxUpper, ni._dMaxUpper, true);
//			}
//			case REPLACE_AVG: {
//				double avg = (ni._dMaxUpper + ni._dMinLower) / 2d;
//				return getDNode(avg, avg, true);
//			}
//			default: {
//				// if (PRUNE_TYPE == REPLACE_RANGE) { // _nWhich == 1
//				// return getDNode(ni._dMinLower, ni._dMinLower, true);
//				// } else if (PRUNE_TYPE == REPLACE_RANGE && _nWhich == 2) {
//				// return getDNode(ni._dMaxUpper, ni._dMaxUpper, true);
//				// } else {
//				// // System.out.println("Illegal replacement type " +
//				// PRUNE_TYPE); // + ", " + _nWhich
//				// Object o1 = null; o1.toString();
//				// }
//				System.out.println("Range replace not implemented yet");
//				System.exit(1);
//			}
//			}
//		}
//
//		// Check cache
//		ADDRNode retc = null;
//		int ret;
//		_tmpADDRNode.set(id);
//		if ((retc = (ADDRNode) _hmPruneMap.get(_tmpADDRNode)) == null) {
//
//			// Get high and low branches for this INode
//			int low = ni._nLow;
//			int high = ni._nHigh;
//
//			// Recurse
//			if (recurse) {
//				low = pruneNodes(low, true);
//				high = pruneNodes(high, true);
//			}
//
//			// Now compute diff at this level
//			double max_abs_diff = Double.POSITIVE_INFINITY;
//			ADDNode adiff = getNode(applyInt(low, high, ARITH_MINUS));
//			if (adiff instanceof ADDINode) {
//				ADDINode adi = (ADDINode) adiff;
//				max_abs_diff = Math.max(Math.abs(adi._dMinLower), Math
//						.abs(adi._dMaxUpper));
//			} else {
//				max_abs_diff = Math.abs(((ADDDNode) adiff)._dLower);
//			}
//
//			// ///////////////// DEBUG ////////////////////
//			// System.out.println("=================================");
//			// System.out.println("Difference: " + max_abs_diff);
//			// System.out.println(getNode(low).toString(this, 0));
//			// System.out.println("---------------------------------");
//			// System.out.println(getNode(high).toString(this, 0));
//			// System.out.println("---------------------------------");
//			// System.out.println(adiff.toString(this, 0));
//
//			// REMOVE!!!
//			// double max_abs_diff2 = Double.POSITIVE_INFINITY;
//			// ADDNode adiff2 = getNode(applyInt(high, low, ARITH_MINUS));
//			// if (adiff2 instanceof ADDINode) {
//			// ADDINode adi = (ADDINode)adiff2;
//			// max_abs_diff2 = Math.max(Math.abs(adi._dMinLower),
//			// Math.abs(adi._dMaxUpper));
//			// } else {
//			// max_abs_diff2 = Math.abs(((ADDDNode)adiff2)._dLower);
//			// }
//			// if (Math.abs(max_abs_diff2 - max_abs_diff) >= 1e-9d) {
//			// System.out.println("Difference: " + max_abs_diff + " / " +
//			// max_abs_diff2);
//			// System.out.println("Assymmetric minus... error!!!");
//			// System.exit(1);
//			// }
//			// System.out.println("=================================");
//			// ////////////////////////////////////////////
//
//			// Should we prune?
//			if ((PRUNE_PRECISION >= 0d) && (max_abs_diff <= PRUNE_PRECISION)) {
//
//				// ///////////////// DEBUG ////////////////////
//				// System.out.println("Pruning type: " + PRUNE_TYPE);
//				// System.out.println("Difference: " + max_abs_diff);
//				// System.out.println("Pruning: \n" + ni.toString(this,0));
//				// System.out.println("---------------------------------");
//				// ////////////////////////////////////////////
//
//				switch (PRUNE_TYPE) {
//				case NO_REPLACE: {
//					ret = getINode(ni._nTestVarID, low, high, true);
//				}
//					break;
//				case REPLACE_LOW: {
//					ret = low;
//				}
//					break;
//				case REPLACE_HIGH: {
//					ret = high;
//				}
//					break;
//				case REPLACE_MIN: {
//					ret = applyInt(low, high, ARITH_MIN);
//				}
//					break;
//				case REPLACE_MAX: {
//					ret = applyInt(low, high, ARITH_MAX);
//				}
//					break;
//				case REPLACE_AVG: {
//					ret = scalarMultiply(applyInt(low, high, ARITH_SUM), 0.5d);
//				}
//					break;
//				default: {
//					// if (PRUNE_TYPE == REPLACE_RANGE) { // && _nWhich == 1
//					// ret = new ADDRNode(applyInt(low, high, ARITH_MIN));
//					// } else if (PRUNE_TYPE == REPLACE_RANGE && _nWhich == 2) {
//					// ret = new ADDRNode(applyInt(low, high, ARITH_MAX));
//					// } else {
//					// System.out.println("Illegal replacement type " +
//					// PRUNE_TYPE); // ", " + _nWhich
//					// Object o1 = null; o1.toString();
//					// }
//					ret = INVALID;
//					System.out.println("Range replace not implemented yet");
//					System.exit(1);
//				}
//				}
//
//				PRECISION_PRUNES++;
//
//			} else {
//
//				// Retrieve the inode
//				ret = getINode(ni._nTestVarID, low, high, true);
//
//			}
//
//			// getINode may return a DNode or BNode if low==high
//			if (getNode(ret) instanceof ADDINode) {
//				setMinMax(ret);
//			}
//
//			// Cache the node in canonical form
//			_hmPruneMap.put(new ADDRNode(id), new ADDRNode(ret));
//
//		} else {
//			PRUNE_CACHE_HITS++;
//			ret = retc._lid;
//		}
//
//		// Return cached value modified by offset
//		return ret;
//	}

	
	
	////////////////////////////////////////////////////////////////////////////
	// Main Computation Algorithms
	////////////////////////////////////////////////////////////////////////////

	private long APRICODDInt(long id) {
		ADDNode node = getNode(id);
		if( node instanceof ADDDNode ){
			return node._nLocalID;
		}else{
			ADDINode inode = (ADDINode)node;
			
			truebr = APRICODDInt(inode._nHigh);
		}
		
	}

	// Assume already built with correct order, just needs reduction
	public int reduce(int root) {
		return reduceRestrict(root, this, -1, -1);
	}

	// Assume already built with correct order, just needs reduction
	public int restrict(int root, int gid, int op) {
		return reduceRestrict(root, this, gid, op);
	}

	// If 'src' is non-null, this will obtain the node structure
	// from the ADD given by src. In this case, the src
	// structure will remain unchanged (used for copying, should
	// only be called if 'this' is empty). TODO: Remove printlns!
	public int reduceRestrict(int id, ADD src, int gid, int op) {
		// Have we examined this node id already?
		// System.out.println("Reduce(" + id + ")");
		ADDRNode qret = null;
		ReduceCacheKey key = new ReduceCacheKey(src, gid, op, id);
		if ((qret = (ADDRNode) _hmReduceMap.get(key)) != null) {
			// System.out.println("In cache, returning: " + qret);
			return qret._lid;
		}

		// Proceed with reduction algorithm
		// System.out.println("Not in cache");
		int ret = INVALID;
		boolean recurse = true;
		ADDNode n = src.getNode(id);

		// Update caches and reduce if needed
		if (n instanceof ADDBNode) {
			ret = getBNode(((ADDBNode) n)._bVal, true);
		} else if (n instanceof ADDDNode) {
			ADDDNode dn = (ADDDNode) n;
			ret = getDNode(dn._dLower, dn._dUpper, true, dn._sLowerLabel,
					dn._sUpperLabel);
		} else { // n instanceof ADDINode so recurse and update caches
			ADDINode ni = (ADDINode) n;

			if (ni._nTestVarID == gid) {

				if (op == RESTRICT_HIGH || op == RESTRICT_LOW) {
					ret = ((op == RESTRICT_LOW) ? reduceRestrict(ni._nLow, src,
							gid, op) : reduceRestrict(ni._nHigh, src, gid, op));
				} else {
					System.out.println("ERROR: op not a RESTRICT!");
					Object o = null;
					o.toString();
					System.exit(1);
				}

			} else {

				// Get new low and high branches
				int low = reduceRestrict(ni._nLow, src, gid, op);
				int high = reduceRestrict(ni._nHigh, src, gid, op);

				// Don't recursively delete if low==high since low
				// will be reused although it may not be linked yet.
				// And we know that low will *have* to be used.
				if (low == high) {
					recurse = false;
				}

				// Decide which node to return (takes care of 'low==high' case)
				// System.out.println("Get:    <" + ni._nGlobalID + "," + low +
				// "," + high + ">");
				ret = getINode(ni._nTestVarID, low, high, true);
				// System.out.println("Result: <" + ni._nGlobalID + "," + low +
				// "," + high + ">  ->  " + ret);

				// getINode may return a DNode or BNode if low==high
				if (getNode(ret) instanceof ADDINode) {
					setMinMax(ret);
				}
			}
		}

		// Cache, update structure, and return. Note: If we came
		// in for a node i and left with j (i != j), then we know
		// every other time we come into i, we will return j so we can
		// completely kill off j. (Only do this if 'src' is 'this' -
		// otherwise we can't compare the node IDs!)
		_hmReduceMap.put(key, new ADDRNode(ret));

		// Note: For both ADD and AADD, reduce() may not completely dec all
		// ref counts, but easier to be conservative for now.

		// if ((id != ret) && (src == this)) {
		// //System.out.println("Alternate reduction of " + id + "(del) to " +
		// ret + "(new)");
		// decRefCount(id, true /* delete! */, recurse /* recursive? */);
		// }
		return ret;
	}

	public int opOut(int rid, int gid, int op) {

		if (op != ARITH_SUM && op != ARITH_PROD && op != ARITH_MAX
				&& op != ARITH_MIN && op != LOG_AND && op != LOG_OR) {
			System.out.println("ERROR: opOut called without SUM/PROD/MIN/MAX");
			Object o = null;
			o.toString();
		}

		// Get high and low branch restrictions for this var
		int high_br = reduceRestrict(rid, this, gid, RESTRICT_HIGH);
		int low_br = reduceRestrict(rid, this, gid, RESTRICT_LOW);

		// Must be called with src b/c nodes will be internalized
		return applyInt(high_br, low_br, op);
	}

	// Remap gids... gid_map = old_id -> new_id (assuming order consistent)
	public int remapGIDsInt(int lid, HashMap node_map) {
		ADDNode n = getNode(lid);
		//System.out.println(lid + ": " + n);
		if (n instanceof ADDBNode || n instanceof ADDDNode) {
			return lid;
		} else { // n instanceof ADDINode so recurse and update caches
			ADDINode ni = (ADDINode) n;
			int oldid = ni._nTestVarID;
			Integer new_id = (Integer)node_map.get(oldid);
			
			if (new_id == null) {
				new_id = ni._nTestVarID;
			}
			
			
			return getINode(new_id.intValue(), remapGIDsInt(ni._nLow, node_map),
					remapGIDsInt(ni._nHigh, node_map), true);
		}
	}

	public int applyInt(int a1, int a2, int op) {
		int ret = getPair(a1, a2, op);
		if (ret > INVALID) {
			return ret;
		}

		// Can we create a terminal node here?
		ADDNode n1 = getNode(a1), n2 = getNode(a2);
		int t = computeTermNode(n1, n2, op);
		if (t > INVALID) {
			ret = t;
		} else { // At least one non-terminal so must recurse

			int v1low, v1high, v2low, v2high, gid;

			// Find node with min id (or only internal node)
			if (n1 instanceof ADDINode) {
				if (n2 instanceof ADDINode) {
					if (comesBefore(((ADDINode) n1)._nTestVarID,
							((ADDINode) n2)._nTestVarID)) {
						gid = ((ADDINode) n1)._nTestVarID;
					} else {
						gid = ((ADDINode) n2)._nTestVarID;
					}
				} else {
					gid = ((ADDINode) n1)._nTestVarID;
				}
			} else {
				gid = ((ADDINode) n2)._nTestVarID;
			}

			// Determine next recursion for n1
			if ((n1 instanceof ADDINode) && (((ADDINode) n1)._nTestVarID == gid)) {
				ADDINode n1i = (ADDINode) n1;
				v1low = n1i._nLow;
				v1high = n1i._nHigh;
			} else {
				v1low = a1;
				v1high = a1;
			}

			// Determine next recursion for n2
			if ((n2 instanceof ADDINode) && (((ADDINode) n2)._nTestVarID == gid)) {
				ADDINode n2i = (ADDINode) n2;
				v2low = n2i._nLow;
				v2high = n2i._nHigh;
			} else {
				v2low = a2;
				v2high = a2;
			}

			// Perform in-line reduction and set min/max for subnodes if needed
			int low = applyInt(v1low, v2low, op);
			int high = applyInt(v1high, v2high, op);

			// getINode will take care of 'low==high'
			ret = getINode(gid, low, high, true);

			// getINode may return a DNode or BNode if low==high
			if (getNode(ret) instanceof ADDINode) {
				setMinMax(ret);
			}
		}

		putPair(a1, a2, op, ret);
		return ret;
	}

	// Computes a terminal node value if possible, assume
	// terms of same type (otherwise incompatible!)
	
	//changed 8/15/11
	//NEGATIVE_INFITY op anything is NEG_INF
	
	public int computeTermNode(ADDNode a1, ADDNode a2, int op) {
//		
//		if( a1 instanceof ADDDNode && ((ADDDNode)a1)._dLower == NEGINF && ((ADDDNode)a1)._dUpper == NEGINF){
//			return getDNode(NEGINF, NEGINF, true);
//		}
//		
//		if( a2 instanceof ADDDNode && ((ADDDNode)a2)._dLower == NEGINF && ((ADDDNode)a2)._dUpper == NEGINF){
//			return getDNode(NEGINF, NEGINF, true);
//		}
		
		int ret = INVALID;

		switch (op) {

		case LOG_AND: 
			if ( ( a1 instanceof ADDDNode ) && ( a2 instanceof ADDDNode ) ) {
				
				ADDDNode a1n = (ADDDNode) a1;
				ADDDNode a2n = (ADDDNode) a2;
				
				boolean v1 = getBoolean(a1n);
				boolean v2 = getBoolean(a2n);
				
				ret = (v1 && v2) ? getDNode(1,1,true) : getDNode(0,0,true);
			}
			break;

		case LOG_OR: 			
			if ( ( a1 instanceof ADDDNode ) && ( a2 instanceof ADDDNode ) ) {
				
				ADDDNode a1n = (ADDDNode) a1;
				ADDDNode a2n = (ADDDNode) a2;
				
				boolean v1 = getBoolean(a1n);
				boolean v2 = getBoolean(a2n);
				
				ret = (v1 || v2) ? getDNode(1,1,true) : getDNode(0,0,true);
			}
			break;

		case ARITH_SUM: {
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				ADDDNode node1 = (ADDDNode) a1;
				ADDDNode node2 = ((ADDDNode) a2);
				
				double min, max ;
				
				if( node1._dLower != NEGINF && node2._dLower != NEGINF ){
					min = node1._dLower + node2._dLower;
				}else{
					min = NEGINF;
				}
				
				if( node1._dUpper!= NEGINF && node2._dUpper != NEGINF ){
					max = node1._dUpper + node2._dUpper;
				}else{
					max = NEGINF;
				}
				
				ret = getDNode(min, max, true);
			}

		}
			break;

		case ARITH_MINUS: {
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				
				ADDDNode node1 = (ADDDNode) a1;
				ADDDNode node2 = ((ADDDNode) a2);
				
				double min , max ;
				
				if( node1._dLower != NEGINF && node2._dLower != NEGINF ){
					min = node1._dLower - node2._dLower;
				}else{
					min = NEGINF;
				}
				
				if( node1._dUpper!= NEGINF && node2._dUpper != NEGINF ){
					max = node1._dUpper - node2._dUpper;
				}else{
					max = NEGINF;
				}
				
				if (min > max) {
					double temp = min;
					min = max;
					max = temp;
				}
				ret = getDNode(min, max, true);
			}

		}
			break;

		case ARITH_DIV: {
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				
				ADDDNode node1 = (ADDDNode) a1;
				ADDDNode node2 = ((ADDDNode) a2);
				
				double min , max ;
				
				if( node1._dLower != NEGINF && node2._dLower != NEGINF ){
					min = node1._dLower / node2._dLower;
				}else{
					min = NEGINF;
				}
				
				if( node1._dUpper!= NEGINF && node2._dUpper != NEGINF ){
					max = node1._dUpper / node2._dUpper;
				}else{
					max = NEGINF;
				}
				
				if (min > max) {
					double temp = min;
					min = max;
					max = temp;
				}
				ret = getDNode(min, max, true);
			}

		}
			break;

		case ARITH_PROD: {
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				
				ADDDNode node1 = (ADDDNode) a1;
				ADDDNode node2 = ((ADDDNode) a2);
				
				double min , max ;
				
				if( node1._dLower != NEGINF && node2._dLower != NEGINF ){
					min = node1._dLower * node2._dLower;
				}else{
					min = NEGINF;
				}

				if( node1._dUpper!= NEGINF && node2._dUpper != NEGINF ){
					max = node1._dUpper * node2._dUpper;
				}else {
					max = NEGINF;
				}
				
				ret = getDNode(min, max, true);
			} else if ((a1 instanceof ADDDNode)
					&& (((ADDDNode) a1)._dLower == (double) 0.0)
					&& (((ADDDNode) a1)._dUpper == (double) 0.0)) {
				// System.out.println("PROD PRUNE!!!"); // TODO: Remove!!!
				PROD_PRUNE_CNT++;
				ret = getDNode((double) 0.0, (double) 0.0, true);
			} else if ((a2 instanceof ADDDNode)
					&& (((ADDDNode) a2)._dLower == (double) 0.0)
					&& (((ADDDNode) a2)._dUpper == (double) 0.0)) {
				// System.out.println("PROD PRUNE!!!"); // TODO: Remove!!!
				PROD_PRUNE_CNT++;
				ret = getDNode((double) 0.0, (double) 0.0, true);
			}
		}
			break;

		case ARITH_MIN: { // Can assume an ADD for arithmetic operations
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				ADDDNode a1d = (ADDDNode) a1;
				ADDDNode a2d = (ADDDNode) a2;
				
				double lower , upper;
				
				if( a1d._dLower != NEGINF && a2d._dLower != NEGINF ){
					lower = Math.min(a1d._dLower, a2d._dLower);
				}else{
					lower = NEGINF;
				}
				
				if( a1d._dUpper != NEGINF && a2d._dUpper != NEGINF ){
					upper = Math.min(a1d._dUpper, a2d._dUpper);
				}else{
					upper = NEGINF;
				}
				
				ret = getDNode(lower, upper, true,
						(lower == a1d._dLower) ? a1d._sLowerLabel
								: a2d._sLowerLabel,
						(upper == a1d._dUpper) ? a1d._sUpperLabel
								: a2d._sUpperLabel);
			} else if ((a1 instanceof ADDDNode) && (a2 instanceof ADDINode)
					&& (((ADDDNode) a1)._dLower <= ((ADDINode) a2)._dMinLower)
					&& (((ADDDNode) a1)._dUpper <= ((ADDINode) a2)._dMinUpper)) {
				// If a1.lower < a2.min.lower && a1.upper < a2.min.upper
				// then can set node to a1
				ADDDNode a1d = (ADDDNode) a1;
				ret = getDNode(a1d._dLower, a1d._dUpper, true,
						a1d._sLowerLabel, a1d._sUpperLabel);
				// System.out.println("MIN PRUNE!!!"); // TODO: Remove!!!
				MIN_PRUNE_CNT++;
			} else if ((a2 instanceof ADDDNode)
					&& (((ADDDNode) a2)._dLower <= ((ADDINode) a1)._dMinLower)
					&& (((ADDDNode) a2)._dUpper <= ((ADDINode) a1)._dMinUpper)) {
				// If a2.lower < a1.min.lower && a2.upper < a1.min.upper
				// then can set node to a2
				ADDDNode a2d = (ADDDNode) a2;
				ret = getDNode(a2d._dLower, a2d._dUpper, true,
						a2d._sLowerLabel, a2d._sUpperLabel);
				// System.out.println("MIN PRUNE!!!"); // TODO: Remove!!!
				MIN_PRUNE_CNT++;
			}
		}
			break;

		case ARITH_MAX: { // Can assume an ADD for arithmetic operations
			if ((a1 instanceof ADDDNode) && (a2 instanceof ADDDNode)) {
				ADDDNode a1d = (ADDDNode) a1;
				ADDDNode a2d = (ADDDNode) a2;
				
				double lower , upper ;
				
				if( a1d._dLower != NEGINF && a2d._dLower != NEGINF ){
					lower = Math.max(a1d._dLower, a2d._dLower);
				}else if( a1d._dLower == NEGINF && a2d._dLower != NEGINF ){
					lower = a2d._dLower;
				}else if( a1d._dLower != NEGINF && a2d._dLower == NEGINF ){
					lower = a1d._dLower;
				}else{
					lower = NEGINF;
				}
				
				if( a1d._dUpper != NEGINF && a2d._dUpper != NEGINF ){
					upper = Math.max(a1d._dUpper, a2d._dUpper);
				}else if( a1d._dUpper == NEGINF && a2d._dUpper != NEGINF ){
					upper = a2d._dUpper;
				}else if( a1d._dUpper != NEGINF && a2d._dUpper == NEGINF ){
					upper = a1d._dUpper;
				}else{
					upper = NEGINF;
				}
				
				ret = getDNode(lower, upper, true,
						(lower == a1d._dLower) ? a1d._sLowerLabel
								: a2d._sLowerLabel,
						(upper == a1d._dUpper) ? a1d._sUpperLabel
								: a2d._sUpperLabel);
			} else if ((a1 instanceof ADDDNode) && (a2 instanceof ADDINode)
					&& (((ADDDNode) a1)._dLower >= ((ADDINode) a2)._dMaxLower)
					&& (((ADDDNode) a1)._dUpper >= ((ADDINode) a2)._dMaxUpper)) {
				// If a1.lower > a2.max.lower && a1.upper > a2.max.upper
				// then can set node to a1
				ADDDNode a1d = (ADDDNode) a1;
				ret = getDNode(a1d._dLower, a1d._dUpper, true,
						a1d._sLowerLabel, a1d._sUpperLabel);
				// System.out.println("MAX PRUNE!!!"); // TODO: Remove!!!
				MAX_PRUNE_CNT++;
			} else if ((a2 instanceof ADDDNode)
					&& (((ADDDNode) a2)._dLower >= ((ADDINode) a1)._dMaxLower)
					&& (((ADDDNode) a2)._dUpper >= ((ADDINode) a1)._dMaxUpper)) {
				// If a2.lower > a1.max.lower && a2.upper > a1.max.upper
				// then can set node to a2
				ADDDNode a2d = (ADDDNode) a2;
				ret = getDNode(a2d._dLower, a2d._dUpper, true,
						a2d._sLowerLabel, a2d._sUpperLabel);
				// System.out.println("MAX PRUNE!!!"); // TODO: Remove!!!
				MAX_PRUNE_CNT++;
			}
		}
			break;
		}

		return ret;
	}

	private boolean getBoolean(ADDDNode a1n) {
		
		if( a1n._dLower == a1n._dUpper ){
			return a1n._dLower == 0 ? false : true;
		}
		
		System.err.println("Not boolean-izable");
		System.exit(1);
		return false;
		
	}

	public static abstract class ADDLeafOperation {
//		public abstract void processADDLeaf(ArrayList<String> assign, double leaf_val);
		public abstract void processADDLeaf(Map<Integer, Boolean> assign,
				double leaf_val);

		public abstract void processADDLeaf(ArrayList<String> assign, double leaf_val);
		
	}

	public void enumeratePaths( int id,
			ADDLeafOperation leaf_op, HashMap<Integer, Boolean> assign ){
		
		Boolean b;
		ADDNode cur = getNode(id);

		if (cur instanceof ADDINode) {
			int level = ((Integer) _hmGVarToLevel.get(new Integer(
					((ADDINode) cur)._nTestVarID))).intValue();
			Integer var_id = (Integer)_alOrder.get(level);
			String var = (String)_hmID2VarName.get(var_id);

			ADDINode ni = (ADDINode) cur;
			assign.put(var_id, false);
			enumeratePaths(ni._nLow, leaf_op, assign);
			assign.put(var_id, true);
			enumeratePaths(ni._nHigh, leaf_op, assign);
			assign.remove(var_id);
			return;
		}
			
		// If get here, cur will be an ADDDNode, ADDBNode
		double leaf_val = Double.NaN;
		if (cur instanceof ADDDNode) {
			leaf_val =  ((ADDDNode) cur)._dLower;
		} else if (cur instanceof ADDBNode) {
			leaf_val =  ((ADDBNode) cur)._bVal ? 1.0d : 0.0d;
		} 
		
		leaf_op.processADDLeaf(assign, leaf_val);
	}
	
	@Deprecated
	public void enumeratePaths(int id, 
			ADDLeafOperation leaf_op, ArrayList<String> assign) {

		Boolean b;
		ADDNode cur = getNode(id);

		if (cur instanceof ADDINode) {
			int level = ((Integer) _hmGVarToLevel.get(new Integer(
					((ADDINode) cur)._nTestVarID))).intValue();
			Integer var_id = (Integer)_alOrder.get(level);
			String var = (String)_hmID2VarName.get(var_id);

			ADDINode ni = (ADDINode) cur;
			assign.add("~" + var);
			enumeratePaths(ni._nLow, leaf_op, assign);
			assign.set(assign.size() - 1, var);
			enumeratePaths(ni._nHigh, leaf_op, assign);
			assign.remove(assign.size() - 1);
			return;
		}
			
		// If get here, cur will be an ADDDNode, ADDBNode
		double leaf_val = Double.NaN;
		if (cur instanceof ADDDNode) {
			leaf_val =  ((ADDDNode) cur)._dLower;
		} else if (cur instanceof ADDBNode) {
			leaf_val =  ((ADDBNode) cur)._bVal ? 1.0d : 0.0d;
		} 
		
		leaf_op.processADDLeaf(assign, leaf_val);
	}
	
	@Override
	public double evaluate(int id, HashMap var2assign) {
		ArrayList assign = new ArrayList();
		for (int i = 0; i <= _alOrder.size(); i++)
			assign.add(null);
		for (Object o : var2assign.entrySet()) {
			Map.Entry me = (Map.Entry)o; 
			int index = (Integer)_hmVarName2ID.get(me.getKey()); // if null, var not in var2ID
			//System.out.println(me.getKey() + " :: " + index + ": " + _hmGVarToLevel);
			int level = (Integer)_hmGVarToLevel.get(index); 
			assign.set(level, (Boolean)me.getValue());
		}
		return evaluate(id, assign);
	}

	// Takes an assignment of gvars->{T|F} (Boolean class) and returns
	// the corresponding terminal node.
	public double evaluate(int id, ArrayList assign) {

		Boolean b;
		ADDNode cur = getNode(id);

		while (cur instanceof ADDINode) {
			int level = ((Integer) _hmGVarToLevel.get(new Integer(
					((ADDINode) cur)._nTestVarID))).intValue();

			// If we need a var this is unassigned, return null
			if ((level < assign.size())
					&& ((b = (Boolean) assign.get(level)) != null)) {
				ADDINode ni = (ADDINode) cur;
				cur = (b.booleanValue()) ? getNode(ni._nHigh)
						: getNode(ni._nLow);
			} else {
				return Double.NaN;
			}
		}

		// If get here, cur will be an ADDDNode, ADDBNode
		if (cur instanceof ADDDNode) {
			return ((ADDDNode) cur)._dLower;
		} else if (cur instanceof ADDBNode) {
			return ((ADDBNode) cur)._bVal ? 1.0d : 0.0d;
		} else {
			return Double.NaN;
		}
	}

	// ///////////////////////////////////////////////////////////////
	// Order maintenance
	// ///////////////////////////////////////////////////////////////

	// Probably have more efficient ways to do a lot of these using
	// binary search and hash tables
	// Order check - both must occur in list!

	public boolean comesBefore(int gid1, int gid2) {
		// Get level for gid1 and gid2
		int l1 = ((Integer) _hmGVarToLevel.get(new Integer(gid1))).intValue();
		int l2 = ((Integer) _hmGVarToLevel.get(new Integer(gid2))).intValue();

		// Determine which comes first (i.e. earlier level)
		return (l1 <= l2);
	}

	// //////////////////////////////////////////////////////////////
	// Construction and File I/O Routines
	// //////////////////////////////////////////////////////////////

	/**
	 * Build an ADD from a list (node is a list, high comes first for internal
	 * nodes)
	 **/
	public int buildDDFromUnorderedTree(ArrayList l) {
		Object o = l.get(0);
		if (o instanceof String && HasOnlyDigits((String) o)) {
			double val = (new BigInteger((String) o)).doubleValue();
			return getDNode(val, val, true);
		} else if (o instanceof BigDecimal) {
			double val = ((BigDecimal) o).doubleValue();
			return getDNode(val, val, true);
		} else {
			String var = (String) o;
			if (((Integer) _hmVarName2ID.get(var)) == null) System.out.println(var);
			int gid = ((Integer) _hmVarName2ID.get(var)).intValue();

			// Get the var ADD
			int high_br = getVarNode(gid, 0.0d, 1.0d);
			high_br = applyInt(high_br, buildDDFromUnorderedTree((ArrayList) l.get(1)) 
					/* high */, ARITH_PROD);

			// Get the !var ADD
			int low_br = getVarNode(gid, 1.0d, 0.0d);
			low_br = applyInt(low_br, buildDDFromUnorderedTree((ArrayList) l.get(2)) 
					/* low */, ARITH_PROD);

			return applyInt(low_br, high_br, ARITH_SUM);
		}
	}

	/**
	 * Build an ADD from a list with correct variable order (node is a list,
	 * high comes first for internal nodes)
	 **/
	public int buildDDFromOrderedTree(ArrayList l) {
		return reduce(buildNode(l));
	}

	public int buildNode(ArrayList l) {

		// System.out.println("Building: " + l);

		Object o = l.get(0);
		if (o instanceof String && HasOnlyDigits((String) o)) {
			double v = (new BigInteger((String) o)).doubleValue();
			return getDNode(v, v, true);
		} else if (o instanceof BigDecimal) {
			double v = ((BigDecimal) o).doubleValue();
			return getDNode(v, v, true);
		} else {
			String var = (String) o;
			int gid = ((Integer) _hmVarName2ID.get(var)).intValue();

			// Get the var ADD
			int high = buildNode((ArrayList) l.get(1));
			int low = buildNode((ArrayList) l.get(2));
			return getINode(gid, low, high, true);
		}
	}

	public static boolean HasOnlyDigits(String s) {
		for (int i = 0; i < s.length(); i++) {
			if (!Character.isDigit(s.charAt(i)) && s.charAt(i) != '-') {
				return false;
			}
		}
		return true;
	}

	public int getVarNode(String var_name, double low, double high) {

		Integer var_gid = (Integer)_hmVarName2ID.get(var_name);
		if (var_gid == null)
			System.err.println("No var ID registered for '" + var_name + "'");
		return getVarNode(var_gid, low, high);
	}

	/** Build a var ADD **/
	public int getVarNode(int gid, double low, double high) {

		int n_low = getDNode(low, low, true);
		int n_high = getDNode(high, high, true);
		return getINode(gid, n_low, n_high, true);
	}

	/** Build a constant ADD */
	public int getConstantNode(double val) {
		return getDNode(val, val, true);
	}
	
	public void exportTree(int n, PrintWriter ps, boolean label_branches) {
		exportTree(n, ps, label_branches ? "" : null, 0);
	}
	
	public void exportTree(int n, PrintWriter ps, boolean label_branches, int level) {
		exportTree(n, ps, label_branches ? "" : null, level);
	}
	
	protected void exportTree(int n, PrintWriter ps, String branch_label, int level) {

		ADDNode cur = getNode(n);

		if (cur instanceof ADDINode) {
			ADDINode i = (ADDINode) cur;
			ps.print("\n" + tab(level) + 
					(branch_label != null && branch_label.length() > 0 ? "(" + branch_label + " " : "") + 
					"(" + _hmID2VarName.get(i._nTestVarID) + " ");
			exportTree(i._nHigh, ps, branch_label != null ? "true" : null, level + 1);
			exportTree(i._nLow, ps, branch_label != null ? "false" : null, level + 1);
			ps.print(branch_label != null && branch_label.length() > 0 ? "))" : ")");
		} else {
			ADDDNode d = (ADDDNode) cur;
			ps.print("\n" + tab(level));
			ps.print((branch_label != null && branch_label.length() > 0 ? "(" + branch_label + " " : ""));
			ps.print("(" + d._dLower + ")");
			ps.print(branch_label != null && branch_label.length() > 0 ? ")" : "");
		}
	}

	public String tab(int len) {
		StringBuffer sb = new StringBuffer();
		for (int i = 0; i < len; i++, sb.append("\t"))
			;
		return sb.toString();
	}

	// //////////////////////////////////////////////////////////////
	// Miscellaneous methods
	// //////////////////////////////////////////////////////////////

	// A quick test to verify canonical order! Returns false if problem.
	public boolean verifyOrder(int id) {
		return verifyOrder(id, -1);
	}

	public boolean verifyOrder(int n, int par_gid) {
		if (n != 0) {
			ADDNode node = getNode(n);
			if (node instanceof ADDDNode) {
				return true;
			}
			ADDINode ni = (ADDINode) node;
			if (par_gid != -1) {
				// Verify order
				if (par_gid == ni._nTestVarID
						|| !comesBefore(par_gid, ni._nTestVarID)) {
					return false;
				}
			}
			return verifyOrder(ni._nLow, ni._nTestVarID)
					&& verifyOrder(ni._nHigh, ni._nTestVarID);
		} else {
			return true;
		}
	}

	public String toString() {

		StringBuffer sb = new StringBuffer();

		// Show order
		sb.append("Var name -> var ID: " + _hmVarName2ID + "\n");
		sb.append("Var order:          " + _alOrder + "\n");

		return sb.toString();
	}

	public Graph getGraph(int id) {
		Graph g = new Graph(true /* directed */, false /* bottom-to-top */,
				false /* left-right */, true /* multi-links */);
		getNode(id).toGraph(this, g);
		g.remap(_hmID2VarName);
		return g;
	}

	public String printNode(int id) {
		return getNode(id).toString(this, 0);
	}

	public void pruneReport() {
		System.out.println("\nPrune Report:\n-------------");
		System.out.println("OR:   " + OR_PRUNE_CNT++);
		System.out.println("AND:  " + AND_PRUNE_CNT++);
		System.out.println("PROD: " + PROD_PRUNE_CNT++);
		System.out.println("MIN:  " + MIN_PRUNE_CNT++);
		System.out.println("MAX:  " + MAX_PRUNE_CNT++ + "\n");
	}

	//Added 8/11/11 - Aswin
	public int AddtoBdd(int dd, double thresh, boolean exact) {

		threshCache.clear();
		int ret = AddtoBddInt(dd, thresh, exact);
		return ret;
		
	}
	
	//if exact... sets leaf value to 1 at the specified thresh value and others to 0
	//if not exact... sets leaf values > thresh to 1 and others to 0
	private int AddtoBddInt(int dd, double thresh, boolean exact ){
		
		Integer cget = threshCache.get(new Pair<Integer, Double>(dd, thresh));
		if( cget != null ) {
			++threshHit ;
			return cget;
		}
		
		ADDNode node = getNode(dd);
		if( node instanceof ADDINode ){
			ADDINode in = (ADDINode)node;
			
			int testvarid = in._nTestVarID;
			
			//prunes based on bounds
			if( !exact ){
				if( in._dMaxUpper <= thresh ) {
					return getConstantNode(0.0d);
				}else if( in._dMinLower > thresh ) {
					//all above
					return getConstantNode(1.0d);
				}
			}

			int high = getVarNode(testvarid, 0.0d, 1.0d);
			int low = getVarNode(testvarid, 1.0d, 0.0d);
			
			//high
			int highbr = AddtoBdd(in._nHigh, thresh, exact);
			
			//low
			int lowbr = AddtoBdd(in._nLow, thresh, exact);
			
			int ret = applyInt( applyInt(high, highbr, DD.ARITH_PROD),
					  applyInt(low, lowbr, DD.ARITH_PROD),
					  DD.ARITH_SUM);
			threshCache.put(new Pair<Integer, Double>(dd, thresh), ret);
			return ret;
			
		}else{
			
			ADDDNode n = (ADDDNode)node;
			if( exact ){
				if( n._dUpper == thresh ){
					return getConstantNode(1.0d);
				}else{
					return getConstantNode(0.0d);
				}
			}else{
				if( n._dUpper > thresh ){
					return getConstantNode(1.0d);
				}else{
					return getConstantNode(0.0d);
				}
			}
				
			
		}
		
	}

	public int align(int dd) {
		alignCache.clear();
		int ret = alignHelper(dd,0);
		alignCache.clear();
		return ret;
	}
	
	private int alignHelper(int dd, int top) {
		
		if( alignCache.get(dd) != null ) {
			return alignCache.get(dd);
		}
		
		ADDNode node = getNode(dd);
		
		if( top == _alOrder.size() || node instanceof ADDDNode ){
			return dd;
		}
		
		
		int id = (Integer)_alOrder.get(top);
//		System.out.println(_hmID2VarName.get(id));
		int truedd = restrict(dd, id, DD.RESTRICT_HIGH);
		int falsedd = restrict(dd, id, DD.RESTRICT_LOW);

		int ret;
		
		if( falsedd == truedd ) {
//			System.out.println("inconsq");
			ret = alignHelper(dd,top+1);
		}else {
			truedd = alignHelper( truedd, top+1);
			falsedd = alignHelper( falsedd , top+1);	
			int truebr = getVarNode(id, 0.0d, 1.0d);
			int falsebr = getVarNode(id, 1.0d, 0.0d);
			
			ret = applyInt(
					applyInt(truedd, truebr, DD.ARITH_PROD),
					applyInt(falsedd, falsebr, DD.ARITH_PROD),
					DD.ARITH_SUM);
		}
		
		alignCache .put(dd, ret);
		
		return ret;
	}

	/**
	 * @param pDLower
	 * @param pDUpper
	 * @return
	 */
	public int getLeafNode(double lower, double upper, String sLowerLabel, String sUpperLabel) {
		int leaf = getConstantNode(lower);
		ADDDNode node = (ADDDNode)getNode(leaf);
		node._dLower = lower;
		node._dUpper = upper;
		node._sLowerLabel = sLowerLabel;
		node._sUpperLabel = sUpperLabel;
		return leaf;
	}

	/**
	 * @param pDd
	 * @param pTmID2VarName
	 * @return
	 */
	public Graph getGraph(int id, Map<Integer, String> VarName2varname) {
		Map<Integer, String> remap = makeNewRemap(VarName2varname);
		
		Graph g = new Graph(true /* directed */, false /* bottom-to-top */,
				false /* left-right */, true /* multi-links */);
		getNode(id).toGraph(this, g);
		
		g.remap(remap);
		
		return g;
	}

	/**
	 * @param pVarName2varname
	 * @return
	 */
	private Map<Integer, String> makeNewRemap(Map<Integer, String> pVarName2varname) {
		Map<Integer, String> ret = new HashMap<Integer, String>();
		Set x = _hmID2VarName.entrySet();
		for( Object entry : x ) {
			Map.Entry<Integer, String> ent = (Map.Entry<Integer, String>)entry;
			int id = ent.getKey();
			String var = String.valueOf(ent.getValue());
			ret.put(id, pVarName2varname.get(Integer.valueOf(var)));
		}
		return ret;
	}

	//constrain operator with quantification 
	//called "restrict" in Somenzi's BDD
	//takes as input a function f and a constraint g
	//f can be ADD
	//g has to be a BDD
	//returns f \doubledownwardarrow g
	public int constrainRestrict(int f, int g) {
		HashSet ConstraintLeaves = new HashSet<Double>();
		collectLeaves(g, ConstraintLeaves );
		for( Object o : ConstraintLeaves ){
			if( !isBoolean((ADDDNode)o) ){
				System.err.println("Constraint is not a BDD?");
				System.exit(1);				
			}
		}
		constrainRestrictCache.clear();
		int ret = constrainRestrictInt(f,g);
		setMinMax(ret);
		return ret;
	}

	private boolean isBoolean(ADDDNode node) {
		if( node._dLower == node._dUpper && ( node._dLower == 0 || node._dUpper == 1 ) ){
			return true;
		}
		return false;
	}

	private int constrainRestrictInt(int f, int g){
		
		if( constrainRestrictCache.get(new Pair<Integer, Integer>(f,g)) == null ){
			
			int DD_ONE = getConstantNode(1.0d);
			int DD_ZERO = getConstantNode(0d);
			int DD_NEG_INF = getConstantNode(NEGINF);
			
			if( getNode(f) instanceof ADDDNode ){
				return ( g == DD_ZERO ) ? DD_NEG_INF : f;
			}else if( g == DD_ONE  || f == g ){
//				System.out.println("Returns f ");
				return f;
			}else if( f == applyInt(DD_ONE, g, DD.ARITH_MINUS) || g == DD_ZERO ){
//				System.out.println("return  neginf");
				return DD_NEG_INF;
			}
			
			//should be internal nodes if here
			ADDINode fNode = (ADDINode) getNode(f);
			ADDINode gNode = (ADDINode) getNode(g);
			
			int v = comesBefore(fNode._nTestVarID, gNode._nTestVarID) ? fNode._nTestVarID : gNode._nTestVarID;
			int ret = -1;
			
			if( v != fNode._nTestVarID && v == gNode._nTestVarID ){//quantify
//				System.out.print("quantifies " + v );
				int quantified = applyInt(gNode._nHigh, gNode._nLow, DD.LOG_OR);
//				if( getGIDs(quantified).contains(v) ){
//					System.err.println("quantify fail");
//					System.exit(1);
//				}d
				ret = constrainRestrictInt(f, quantified);
			}else if( v == fNode._nTestVarID && v != gNode._nTestVarID ){
//				System.out.print(" recurse " + v);
				//recurse
				int high = constrainRestrictInt(fNode._nHigh, g);
				int low = constrainRestrictInt(fNode._nLow, g);
				
				int highbr = getVarNode(fNode._nTestVarID, 0.0d, 1.0d);
				highbr = ( high == DD_NEG_INF ) ? getVarNode(fNode._nTestVarID, 0.0d, NEGINF) : applyInt(highbr, high, DD.ARITH_PROD);
				
				int lowbr = getVarNode(fNode._nTestVarID, 1.0d, 0.0d);
				lowbr = ( low == DD_NEG_INF ) ? getVarNode(fNode._nTestVarID, NEGINF, 0.0d) : applyInt(lowbr, low, DD.ARITH_PROD);
				
				ret = applyInt(
						lowbr, highbr,
						DD.ARITH_SUM);
				
			}else if( v == fNode._nTestVarID && v == gNode._nTestVarID ){
//				System.out.print("recurse on both " + v + " ");
				//recurse on both
				int high = constrainRestrictInt(fNode._nHigh, gNode._nHigh);
				int low = constrainRestrictInt(fNode._nLow, gNode._nLow);
				
				int highbr = getVarNode(fNode._nTestVarID, 0.0d, 1.0d);
				highbr = ( high == DD_NEG_INF ) ? getVarNode(fNode._nTestVarID, 0.0d, NEGINF) : applyInt(highbr, high, DD.ARITH_PROD);
				
				int lowbr = getVarNode(fNode._nTestVarID, 1.0d, 0.0d);
				lowbr = ( low == DD_NEG_INF ) ? getVarNode(fNode._nTestVarID, NEGINF, 0.0d) : applyInt(lowbr, low, DD.ARITH_PROD);
				
				ret = applyInt(
						lowbr, highbr,
						DD.ARITH_SUM);
				
			}
			
			constrainRestrictCache.put(new Pair<Integer, Integer>(f,g), ret);
		}else{
			++constrainHit ;
		}
		
		return constrainRestrictCache.get(new Pair<Integer, Integer>(f, g));
		
	}
	
}
